YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add following weak dependency pairs: Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#2^#(nil(), @x) -> c_5() , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , group3#3^#(nil(), @x, @y) -> c_7() , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } and mark the set of starting terms. We apply the transformation 'usablerules' on the sub-problem: Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#2^#(nil(), @x) -> c_5() , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , group3#3^#(nil(), @x, @y) -> c_7() , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } Strict Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We apply the transformation 'weightgap of dimension 2, cbits 3' on the sub-problem: Strict DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#2^#(nil(), @x) -> c_5() , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , group3#3^#(nil(), @x, @y) -> c_7() , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } StartTerms: basic terms Strategy: innermost The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_6) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1} TcT has computed following constructor-restricted matrix interpretation. [::](x1, x2) = [1 0] x2 + [0] [0 0] [0] [nil] = [0] [0] [tuple#3](x1, x2, x3) = [0] [0] [group3^#](x1) = [2] [0] [c_1](x1) = [1 0] x1 + [0] [0 1] [0] [group3#1^#](x1) = [0] [0] [c_2](x1) = [1 0] x1 + [0] [0 1] [0] [group3#2^#](x1, x2) = [0] [0] [c_3] = [0] [0] [c_4](x1) = [1 0] x1 + [0] [0 1] [0] [group3#3^#](x1, x2, x3) = [0] [0] [c_5] = [0] [0] [c_6](x1) = [1 0] x1 + [2] [0 1] [0] [c_7] = [0] [0] [zip3^#](x1, x2, x3) = [1 0] x1 + [0 0] x2 + [1 0] x3 + [2] [0 0] [2 0] [2 2] [2] [c_8](x1) = [1 0] x1 + [0] [0 1] [0] [zip3#1^#](x1, x2, x3) = [1 0] x1 + [1 0] x3 + [0] [0 0] [2 2] [0] [c_9](x1) = [1 0] x1 + [0] [0 1] [0] [zip3#2^#](x1, x2, x3, x4) = [1 0] x2 + [1 0] x4 + [0] [0 0] [2 2] [0] [c_10] = [0] [0] [c_11](x1) = [1 0] x1 + [0] [0 1] [0] [zip3#3^#](x1, x2, x3, x4, x5) = [1 0] x1 + [1 0] x3 + [0 0] x5 + [0] [0 0] [0 0] [2 0] [0] [c_12] = [0] [0] [c_13](x1) = [1 0] x1 + [2] [0 1] [2] [c_14] = [0] [0] This order satisfies following ordering constraints Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#2^#(nil(), @x) -> c_5() , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , group3#3^#(nil(), @x, @y) -> c_7() , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {4,5,6,10,11,12} by applications of Pre({4,5,6,10,11,12}) = {1,3,7,9}. Here rules are labeled as follows: DPs: { 1: group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , 2: group3#1^#(nil()) -> c_3() , 3: group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , 4: group3#2^#(nil(), @x) -> c_5() , 5: group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , 6: group3#3^#(nil(), @x, @y) -> c_7() , 7: zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , 8: zip3#1^#(nil(), @l2, @l3) -> c_10() , 9: zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , 10: zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , 11: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , 12: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() , 13: group3^#(@l) -> c_1(group3#1^#(@l)) , 14: zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#2^#(nil(), @x) -> c_5() , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , group3#3^#(nil(), @x, @y) -> c_7() , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {3,6} by applications of Pre({3,6}) = {1,4}. Here rules are labeled as follows: DPs: { 1: group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , 2: group3#1^#(nil()) -> c_3() , 3: group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , 4: zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , 5: zip3#1^#(nil(), @l2, @l3) -> c_10() , 6: zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , 7: group3^#(@l) -> c_1(group3#1^#(@l)) , 8: group3#2^#(nil(), @x) -> c_5() , 9: group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , 10: group3#3^#(nil(), @x, @y) -> c_7() , 11: zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , 12: zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , 13: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , 14: zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#2^#(nil(), @x) -> c_5() , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , group3#3^#(nil(), @x, @y) -> c_7() , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { group3#2^#(nil(), @x) -> c_5() , group3#3^#(nil(), @x, @y) -> c_7() , zip3#2^#(nil(), @l3, @x, @xs) -> c_12() , zip3#3^#(nil(), @x, @xs, @y, @ys) -> c_14() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component: Problem (R): ------------ Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } StartTerms: basic terms Strategy: innermost Problem (S): ------------ Strict DPs: { zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } StartTerms: basic terms Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } StartTerms: basic terms Strategy: innermost This problem was proven YES(O(1),O(n^1)). S) Strict DPs: { zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } StartTerms: basic terms Strategy: innermost This problem was proven YES(O(1),O(n^1)). Proofs for generated problems: ------------------------------ R) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: group3#1^#(nil()) -> c_3() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_6) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [::](x1, x2) = [1] x2 + [0] [nil] = [2] [tuple#3](x1, x2, x3) = [0] [group3^#](x1) = [2] x1 + [0] [c_1](x1) = [1] x1 + [0] [group3#1^#](x1) = [2] x1 + [0] [c_2](x1) = [1] x1 + [0] [group3#2^#](x1, x2) = [2] x1 + [0] [c_3] = [0] [c_4](x1) = [1] x1 + [0] [group3#3^#](x1, x2, x3) = [2] x1 + [0] [c_6](x1) = [1] x1 + [0] [zip3^#](x1, x2, x3) = [0] [c_8](x1) = [0] [zip3#1^#](x1, x2, x3) = [0] [c_9](x1) = [0] [zip3#2^#](x1, x2, x3, x4) = [0] [c_10] = [0] [c_11](x1) = [0] [zip3#3^#](x1, x2, x3, x4, x5) = [0] [c_13](x1) = [0] This order satisfies following ordering constraints [group3^#(@l)] = [2] @l + [0] >= [2] @l + [0] = [c_1(group3#1^#(@l))] [group3#1^#(::(@x, @xs))] = [2] @xs + [0] >= [2] @xs + [0] = [c_2(group3#2^#(@xs, @x))] [group3#1^#(nil())] = [4] > [0] = [c_3()] [group3#2^#(::(@y, @ys), @x)] = [2] @ys + [0] >= [2] @ys + [0] = [c_4(group3#3^#(@ys, @x, @y))] [group3#3^#(::(@z, @zs), @x, @y)] = [2] @zs + [0] >= [2] @zs + [0] = [c_6(group3^#(@zs))] The strictly oriented rules are moved into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { group3#1^#(nil()) -> c_3() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , 2: group3^#(@l) -> c_1(group3#1^#(@l)) , 4: group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_6) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [::](x1, x2) = [1] x2 + [2] [nil] = [0] [tuple#3](x1, x2, x3) = [0] [group3^#](x1) = [2] x1 + [2] [c_1](x1) = [1] x1 + [0] [group3#1^#](x1) = [2] x1 + [0] [c_2](x1) = [1] x1 + [0] [group3#2^#](x1, x2) = [2] x1 + [0] [c_3] = [0] [c_4](x1) = [1] x1 + [2] [group3#3^#](x1, x2, x3) = [2] x1 + [2] [c_6](x1) = [1] x1 + [0] [zip3^#](x1, x2, x3) = [0] [c_8](x1) = [0] [zip3#1^#](x1, x2, x3) = [0] [c_9](x1) = [0] [zip3#2^#](x1, x2, x3, x4) = [0] [c_10] = [0] [c_11](x1) = [0] [zip3#3^#](x1, x2, x3, x4, x5) = [0] [c_13](x1) = [0] This order satisfies following ordering constraints [group3^#(@l)] = [2] @l + [2] > [2] @l + [0] = [c_1(group3#1^#(@l))] [group3#1^#(::(@x, @xs))] = [2] @xs + [4] > [2] @xs + [0] = [c_2(group3#2^#(@xs, @x))] [group3#2^#(::(@y, @ys), @x)] = [2] @ys + [4] >= [2] @ys + [4] = [c_4(group3#3^#(@ys, @x, @y))] [group3#3^#(::(@z, @zs), @x, @y)] = [2] @zs + [6] > [2] @zs + [2] = [c_6(group3^#(@zs))] Consider the set of all dependency pairs DPs: { 1: group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , 2: group3^#(@l) -> c_1(group3#1^#(@l)) , 3: group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , 4: group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1,2,4}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded S) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() } Weak DPs: { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) , zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { group3^#(@l) -> c_1(group3#1^#(@l)) , group3#1^#(::(@x, @xs)) -> c_2(group3#2^#(@xs, @x)) , group3#1^#(nil()) -> c_3() , group3#2^#(::(@y, @ys), @x) -> c_4(group3#3^#(@ys, @x, @y)) , group3#3^#(::(@z, @zs), @x, @y) -> c_6(group3^#(@zs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#1^#(nil(), @l2, @l3) -> c_10() } Weak DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: zip3#1^#(nil(), @l2, @l3) -> c_10() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [::](x1, x2) = [1] x2 + [0] [nil] = [2] [tuple#3](x1, x2, x3) = [0] [group3^#](x1) = [0] [c_1](x1) = [0] [group3#1^#](x1) = [0] [c_2](x1) = [0] [group3#2^#](x1, x2) = [0] [c_3] = [0] [c_4](x1) = [0] [group3#3^#](x1, x2, x3) = [0] [c_6](x1) = [0] [zip3^#](x1, x2, x3) = [2] x1 + [0] [c_8](x1) = [1] x1 + [0] [zip3#1^#](x1, x2, x3) = [2] x1 + [0] [c_9](x1) = [1] x1 + [0] [zip3#2^#](x1, x2, x3, x4) = [2] x4 + [0] [c_10] = [1] [c_11](x1) = [1] x1 + [0] [zip3#3^#](x1, x2, x3, x4, x5) = [2] x3 + [0] [c_13](x1) = [1] x1 + [0] This order satisfies following ordering constraints [zip3^#(@l1, @l2, @l3)] = [2] @l1 + [0] >= [2] @l1 + [0] = [c_8(zip3#1^#(@l1, @l2, @l3))] [zip3#1^#(::(@x, @xs), @l2, @l3)] = [2] @xs + [0] >= [2] @xs + [0] = [c_9(zip3#2^#(@l2, @l3, @x, @xs))] [zip3#1^#(nil(), @l2, @l3)] = [4] > [1] = [c_10()] [zip3#2^#(::(@y, @ys), @l3, @x, @xs)] = [2] @xs + [0] >= [2] @xs + [0] = [c_11(zip3#3^#(@l3, @x, @xs, @y, @ys))] [zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys)] = [2] @xs + [0] >= [2] @xs + [0] = [c_13(zip3^#(@xs, @ys, @zs))] The strictly oriented rules are moved into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Strict DPs: { zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) } Weak DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(nil(), @l2, @l3) -> c_10() , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { zip3#1^#(nil(), @l2, @l3) -> c_10() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) } Weak DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , 3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [::](x1, x2) = [1] x2 + [2] [nil] = [0] [tuple#3](x1, x2, x3) = [0] [group3^#](x1) = [0] [c_1](x1) = [0] [group3#1^#](x1) = [0] [c_2](x1) = [0] [group3#2^#](x1, x2) = [0] [c_3] = [0] [c_4](x1) = [0] [group3#3^#](x1, x2, x3) = [0] [c_6](x1) = [0] [zip3^#](x1, x2, x3) = [2] x2 + [1] x3 + [2] [c_8](x1) = [1] x1 + [0] [zip3#1^#](x1, x2, x3) = [2] x2 + [1] x3 + [0] [c_9](x1) = [1] x1 + [0] [zip3#2^#](x1, x2, x3, x4) = [2] x1 + [1] x2 + [0] [c_10] = [0] [c_11](x1) = [1] x1 + [2] [zip3#3^#](x1, x2, x3, x4, x5) = [1] x1 + [2] x5 + [1] [c_13](x1) = [1] x1 + [0] This order satisfies following ordering constraints [zip3^#(@l1, @l2, @l3)] = [2] @l2 + [1] @l3 + [2] > [2] @l2 + [1] @l3 + [0] = [c_8(zip3#1^#(@l1, @l2, @l3))] [zip3#1^#(::(@x, @xs), @l2, @l3)] = [2] @l2 + [1] @l3 + [0] >= [2] @l2 + [1] @l3 + [0] = [c_9(zip3#2^#(@l2, @l3, @x, @xs))] [zip3#2^#(::(@y, @ys), @l3, @x, @xs)] = [1] @l3 + [2] @ys + [4] > [1] @l3 + [2] @ys + [3] = [c_11(zip3#3^#(@l3, @x, @xs, @y, @ys))] [zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys)] = [2] @ys + [1] @zs + [3] > [2] @ys + [1] @zs + [2] = [c_13(zip3^#(@xs, @ys, @zs))] Consider the set of all dependency pairs DPs: { 1: zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , 2: zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , 3: zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , 4: zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {2,3,4}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { zip3^#(@l1, @l2, @l3) -> c_8(zip3#1^#(@l1, @l2, @l3)) , zip3#1^#(::(@x, @xs), @l2, @l3) -> c_9(zip3#2^#(@l2, @l3, @x, @xs)) , zip3#2^#(::(@y, @ys), @l3, @x, @xs) -> c_11(zip3#3^#(@l3, @x, @xs, @y, @ys)) , zip3#3^#(::(@z, @zs), @x, @xs, @y, @ys) -> c_13(zip3^#(@xs, @ys, @zs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))